Бабкин Эдуард Александрович - кандидат технических наук, PhD in Computer Science, профессор кафедры информационных систем и технологий, факультет бизнес-информатики и прикладной математики, Национальный исследовательский университет «Высшая школа экономики» 
Адрес: 603155, г. Нижний Новгород, ул. Б.Печерская, д. 25/12
E-mail: eababkin@hse.ru

Бузуева Анна Александровна - студент кафедры информационных систем и технологий, факультет бизнес-информатики и прикладной математики, Национальный исследовательский университет «Высшая школа экономики» 
Адрес: 603155, г. Нижний Новгород, ул. Б.Печерская, д. 25/12
E-mail: anna.a.buzueva@gmail.com

Логвинова Кира Владимировна -кандидат физико-математических наук, PhD in Mathematics, профессор кафедры информационных систем и технологий, факультет бизнес-информатики и прикладной математики, Национальный исследовательский университет «Высшая школа экономики» 
Адрес: 603155, г. Нижний Новгород, ул. Б.Печерская, д. 25/12
E-mail: klogvinova@hse.ru

      В статье рассматривается проблема обнаружения логических противоречий в моделях бизнес-процессов и предлагается способ решения этой проблемы с иллюстрацией на примере анализа сложных бизнес-процессов системы здравоохранения на основе формального подхода реляционной логики. Предлагаемый способ должен способствовать повышению эффективности управления муниципальными учреждениями здравоохранения прежде всего в аспекте повышения качества предоставления комплексных услуг для лиц пожилого возраста. Предлагаемый метод основан на формальных инструментах реляционной логики системы моделирования MIT Alloy Analyzer. Для моделирования бизнес-процессов был выбран перспективный подход онтологии организации и конкретная методология моделирования DEMO (Design & Engineering Methodology for Organizations). Эта методология дает возможность полного и объективного описания организации и функционирования современного предприятия. Анализ построенных по методологии DEMO моделей организации позволяет получить детальное представление о процессах управления и взаимодействия и служит основой для проведения бизнес-реинжиниринга и развития информационной инфраструктуры, согласованной с требованиями бизнеса. Важной частью нашего исследования является разработка формальных спецификаций построенных моделей бизнес-процессов, пригодных для применения формальных методов верификации. Поэтому с целью повторного использования разработанных нами методов трансляции моделей бизнес-процессов на язык системы Alloy Analyzer была создана метамодель ключевых конструктивных элементов методологии моделирования DEMO.
       На основе разработанной мета-модели и конкретных бизнес-процессов предоставления медицинских услуг в ходе исследования были построены формальные модели и проведен анализ их логической непротиворечивости в том числе и во временном аспекте.